event-system0{i:l}  Type{i'} 

latex

Definitions	t  T, f(a), x:A. B(x), isrcv(k), b, True, T, P  Q, x:AB(x), SqStable(P), {x:A| B(x) }, Top, Type, Id, Knd, IdLnk, x,y. t(x;y), x. t(x), kindcase(k; a.f(a); l,t.g(l;t) ), x.A(x), ESAtomAxiom{i:l}(T;V), x:AB(x), ESAxioms(E;T;M;loc;kind;val;when;after;sends;sender;index;first;pred;causl), Prop, A, , lnk(k), Msg_sub(l;M), ||as||, #$n, {i..j}, type List, eventtype(k;loc;V;M;e), EqDecider(T), ES0
Lemmas	deq wf, eventtype wf, int seg wf, length wf1, Msg sub wf, lnk wf, bool wf, not wf, ESAxioms wf, ESAtomAxiom wf, kindcase wf, IdLnk wf, Knd wf, Id wf, top wf, sq stable from decidable, decidable assert, assert wf, isrcv wf